There are other good reasons for finding an alternative microkernel to Mach.
The precompiled kernel distributed with the 0.2 release of the GNU system is 1162k. Admittedly, this contains a large number of device drivers and it is possible to build a kernel specific to a particular machine which will contain only the appropriate device drivers and so will be smaller. However, the Linux (version 2.0.33) kernel I have on my PC is only 1055k, and that includes most of the functionality which must then be deployed by additional servers on top of Mach.
Recent measurements [#!muperf!#] show the performance of Mach to be dramatically less than previously reported. In particular, comparing IPC performance between monolithic and Mach-based systems shows closer to 50% performance rather than the 90% often claimed.
Mach contains in excess of 200 system calls. The semantics of each call are complex and several of them would be better implemented without (direct) kernel intervention. For example, many of the vm_* interfaces could be directly implemented as an IPC from the task to its memory manager. The OSF Mach Kernel Interfaces document is in excess of 450 pages.
The L4 microkernel seems to suffer from none of these faults. L4 running on the x86 family is under 32k and outperforms Mach by a significant factor. It contains just 7 system calls and the reference manual is only 50 pages. It does not contain a default memory pager as Mach does, but I do not see this as a disadvantage since different operating systems have such different requirements for a pager that they normally provide their own in any case.
L4 is available for the Intel 486 (and compatible CPUs) and MIPS processors. A version for the DEC Alpha is in development. Some interest has been expressed in a version for the ARM.